/*
 * Copyright 2012 Christian Schindelhauer, Peter Thiemann, Faisal Aslam, Luminous Fennell and Gidon Ernst.
 * All Rights Reserved.
 * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER
 * 
 * This code is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License version 3
 * only, as published by the Free Software Foundation.
 * 
 * This code is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 * General Public License version 3 for more details (a copy is
 * included in the LICENSE file that accompanied this code).
 * 
 * You should have received a copy of the GNU General Public License
 * version 3 along with this work; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
 * 02110-1301 USA
 * 
 * Please contact Faisal Aslam 
 * (faisal.aslam AT gmail.com)
 * if you need additional information or have any questions.
 */
package takatuka.verifier.logic.DFA;

import java.util.*;
import takatuka.classreader.dataObjs.*;
import takatuka.verifier.dataObjs.*;
import takatuka.verifier.dataObjs.attribute.*;
import takatuka.classreader.dataObjs.attribute.*;
import takatuka.classreader.logic.factory.*;
import takatuka.util.*;
import takatuka.verifier.logic.factory.*;
import takatuka.classreader.logic.util.*;
import takatuka.lineNumberRec.*;

/**
 * <p>Title: </p>
 * <p>Description:
 * This is part of Pass-3 and based on http://java.sun.com/docs/books/jvms/second_edition/html/ClassFile.doc.html#9801
 * (i.e. Section 4.9.2 later half).
 * It operate as follows.
 * INITIALIZATION
 * 1. For the first instruction.
 *    --- For the first instruction of the method, the local variables that represent parameters initially
 *    contain values of the types indicated by the method's ret descriptor; the operand stack is empty.
 *    All other local variables contain an illegal value.
 * 2. For the other instructions, which have not been examined yet,
 *    no information is available regarding the operand stack or local variables.
 * 3. Initially "change-bit" of first instruction is set and all other instruction un-set.
 *   For each instruction, a corresponding "changed" bit indicates whether this instruction needs
 *   to be looked at.
 *
 * EXECUTION
 * 1. Select a virtual machine instruction whose "changed" bit is set. If no instruction
 *    remains whose "changed" bit is set, the method has successfully been verified.
 *    Otherwise, turn off the "changed" bit of the selected instruction.
 * 2. Model the effect of the instruction on the operand stack and local variable array by doing the following:
 * (A) If the instruction uses values from the operand stack, ensure that there are a sufficient number of values
on the stack and that the top values on the stack are of an appropriate ret. Otherwise, verification fails.
 * (B) If the instruction uses a local variable, ensure that the specified local variable contains a value of the
appropriate ret. Otherwise, verification fails.
 * (C) If the instruction pushes values onto the operand stack, ensure that there is sufficient room on the operand
stack for the new values. Add the indicated types to the top of the modeled operand stack.
 * (D) If the instruction modifies a local variable, record that the local variable now contains the new ret.
 * 3. Determine the instructions that can follow the current instruction. Successor instructions can be one of the following:
 * (A) The next instruction, if the current instruction is not an unconditional control transfer instruction
(for instance goto, return, or athrow). Verification fails if it is possible to "fall off" the last instruction of the method.
 * (B) The target(s) of a conditional or unconditional branch or switch.
 * (C) Any exception handlers for this instruction.
 * 4. Merge the state of the operand stack and local variable array at the end of the execution
 *    of the current instruction into each of the successor instructions.
 *    In the special case of control transfer to an exception handler, the operand stack
 *    is set to contain a single object of the exception ret indicated by the exception handler information.
 *    If this is the first time the successor instruction has been visited, record that the operand stack and
 *    local variable values calculated in steps 2 and 3 are the state of the operand stack and local variable
 *    array prior to executing the successor instruction. Set the "changed" bit for the successor instruction.
 *
 *    If the successor instruction has been seen before, merge the operand stack and local variable values
 *    calculated in steps 2 and 3 into the values already there. Set the "changed" bit if there is any
 *    modification to the values.
 *
 * </p>
 * @author Faisal Aslam
 * @version 1.0
 */
public class DataFlowAnalyzer {

    private final static DataFlowAnalyzer dataFlowAnalyzer = new DataFlowAnalyzer();
    protected static Oracle oracle = Oracle.getInstanceOf();
    private FactoryFacade factory =
            FactoryPlaceholder.getInstanceOf().getFactory();
    public static boolean shouldDebugPrint = false;
    private static BytecodeVerifier lastBytecodeVerifier = null;
    private Frame lastExeMethodFrame = null;
    private static VerificationInstruction lastInstrExecuted = null;
    private HashMap<MethodInfo, HashSet<Integer>> excepTableEntriesUsedPerMethod = new HashMap<MethodInfo, HashSet<Integer>>();

    protected DataFlowAnalyzer() {
        super();
    }

    public static DataFlowAnalyzer getInstanceOf() {
        return dataFlowAnalyzer;
    }

    public static void Debug_print(Object obj1, Object obj2, Object obj3, Object obj4, Object obj5) {
        if (shouldDebugPrint) {
            Miscellaneous.println(obj1 + "" + obj2 + "" + obj3 + "" + obj4 + "" + obj5);
        }
    }

    public static void Debug_print(Object obj1, Object obj2) {
        if (shouldDebugPrint) {
            Miscellaneous.println(obj1 + "" + obj2);
        }
    }

    public static void Debug_print1(Object obj1) {
        if (shouldDebugPrint) {
            Miscellaneous.println(obj1);
        }
    }

    /**
     * Check that code does not end at the middle of an instruction. By following steps.
     * 1. Check the code length and code array length is same.
     * 2. Check that last instruction is properly completed.
     *
     * @param attribute CodeAtt
     * @return boolean
     */
    private boolean codeEndVerifier(CodeAtt attribute) {
        //todo
        return false;
    }

    /**
     * For each exception handler, the starting and ending point of code protected by
     * the handler must be at the beginning of an instruction or, in the case of the
     * ending point, immediately past the end of the code. The starting point must be
     * before the ending point.
     * The exception handler code must start at a valid instruction, and it may not start
     * at an opcode being modified by the wide instruction.
     *
     * @param attribute CodeAtt
     * @return boolean
     */
    private boolean checkInstructionHandler(CodeAtt attribute) {
        //todo
        return false;
    }

    /**
     * If the method is already been invoked at least once before then it is not invoked again.
     * There are two cases
     * 
     * case 1: Method is still under execution. If so than a dummy return is added in the caller stack
     * and the call is returned. 
     * **** Note that later on this dummy return must be replace with the actual return when
     * the original method is returns.
     * Furthermore, if the method is native (has no codeAttribute) then it is also executed virtually.
     * 
     * case 2: In case the method had eneded its execution then the return value of the previous call 
     * is saved in the caller return.
     *
     * @param methodputField
     * @param localVariables
     * @param callerStack
     * @return
     * true if the method is executed virtually otherwise return false.
     */
    protected boolean executeVirtually(MethodInfo method, Vector localVariables,
            OperandStack callerStack) {
        return false;
    }

    protected void workBeforeMethodExecuted(MethodInfo method,
            Vector localVariables,
            OperandStack callerStack,
            VerificationInstruction lastInstrExecuted) {
    }

    /**
     * Starts the data-flow-analyzer on the code attributes of the function
     * 
     * @param method
     * @param localVariables
     * In case method is called from another method then one can pass localVariables
     * otherwise just give it null value
     * @param callerStack
     * Similarly, callerStack is required as a method might return a value.
     */
    public void execute(MethodInfo method, Vector localVariables,
            OperandStack callerStack) {
        VerificationFrameFactory frameFactory = FrameFactoryPlaceHolder.getInstanceOf().getFactory();
        String methodString = oracle.getMethodOrFieldString(method);
        try {
            if (executeVirtually(method, localVariables, callerStack)) {
                return;
            }

            workBeforeMethodExecuted(method, localVariables, callerStack, lastInstrExecuted);

            //clear any already existing frame from the method instructions.
            clearMethodOldFrames(method);
            //INITIALIZATION
            Frame frame = InitializeFirstInstruction.createFrameAndInitFirstInstr(method, localVariables);
            LocalVariables locaVar = frame.getLocalVariables();
            Vector callingParameters = (Vector) locaVar.getAll().clone();
            lastBytecodeVerifier = frameFactory.createBytecodeVerifier(frame, method, callingParameters);
            if (frame != null && shouldMethodExecute(method, localVariables, callerStack)) {

                if (methodString.contains("testException")) {
                    //System.out.println("Stop here");
                    //shouldDebugPrint = true;
                }
                Debug_print("\n---------------------------- Class Name = ",
                        ClassFile.currentClassToWorkOn.getFullyQualifiedClassName());
                Debug_print(" method = " + oracle.getMethodOrFieldString(method),
                        ", method NaTIndex=" + method.getNameIndex() + ", " + method.getDescriptorIndex());
                Debug_print("\n\n\tOperandStack after initiliation ", frame.getOperandStack());
                Debug_print("\tLocalVariables after initiliation ", frame.getLocalVariables());
                //done with initilization and now executeInstructions verification on the method
                executeInstructions(lastBytecodeVerifier, callerStack, localVariables);
            } else {
                Debug_print1("************ Method has been execute before and is not executed again or has no instructions");
            }
            workAfterMethodExecuted(method, frame, callerStack,
                    lastBytecodeVerifier.getReturnType(),
                    callingParameters);
        } catch (Exception d) {
            d.printStackTrace();
            Miscellaneous.exit();
        }
    }

    /**
     * execute-force a method even if that is executed before and may be executed from the middle instead of
     * a first instruction.
     *
     * @param method
     * @param localVariables
     * @param callerStack
     * @param bytecodeVerifier
     */
    public void executeForce(MethodInfo method, Vector localVariables,
            OperandStack callerStack, BytecodeVerifier bytecodeVerifier) {
        try {
            Frame frame = bytecodeVerifier.getFrame();
            Vector callingParameters = bytecodeVerifier.getMethodCallingParameters();
            executeInstructions(bytecodeVerifier, callerStack, localVariables);
            /*GCType retType = FunctionStateRecorder.getInstanceOf().
            getFunctionReturnType(method, localVariables);
            if (retType != null) {
            lastBytecodeVerifier.addReturnType(retType);
            }*/
            workAfterMethodExecuted(method, frame, callerStack,
                    lastBytecodeVerifier.getReturnType(),
                    callingParameters);

        } catch (Exception d) {
            d.printStackTrace();
            Miscellaneous.exit();
        }
    }

    public static BytecodeVerifier getLastSavedBytecodeInterpreter() {
        return lastBytecodeVerifier;
    }

    protected Type mergeReturnReferences(HashSet<Type> retTypeSet) {
        Type ret = null;
        VerificationFrameFactory frameFactory = FrameFactoryPlaceHolder.getInstanceOf().getFactory();
        try {
            Iterator<Type> it = retTypeSet.iterator();

            while (it.hasNext()) {
                OperandStack dummyStack = frameFactory.createOperandStack(0);
                if (ret == null) {
                    ret = it.next();
                } else {
                    ret = dummyStack.mergeReferences(ret, it.next());
                }
            }
        } catch (Exception d) {
            d.printStackTrace();
            Miscellaneous.exit();
        }
        return ret;
    }

    protected Type mergeReturnTypes(HashSet<Type> retTypeSet) {
        Iterator<Type> retTypeIt = retTypeSet.iterator();
        while (retTypeIt.hasNext()) {
            Type retType = retTypeIt.next();
            if (!retType.isReference() || retTypeSet.size() == 1) {
                return retType;
            } else {
                return mergeReturnReferences(retTypeSet);
            }
        }
        return null;
    }

    /**
     * 
     * @return
     */
    public Frame getLastExecutedMethodFrame() {
        return lastExeMethodFrame;
    }

    protected void workAfterMethodExecuted(MethodInfo method,
            Frame myFrame, OperandStack callerStack,
            HashSet<Type> returnTypes,
            Vector methodCallingParameters) throws Exception {
        printFramesOfTheWholeMethod(method);
        Type returnType = mergeReturnTypes(returnTypes);
        if (returnType != null && callerStack != null) {
            callerStack.push(returnType);
        }
        lastExeMethodFrame = myFrame;
    }

    public void printFramesOfTheWholeMethod(MethodInfo method) {
        if (!shouldDebugPrint) {
            return;
        }
        Debug_print1("\n\n******** Summary of the whole method ********* ");
        Debug_print("method = ", oracle.getMethodOrFieldString(method));
        Vector instrs = method.getCodeAtt().getInstructions();
        for (int loop = 0; loop < instrs.size(); loop++) {
            VerificationInstruction specialInst = (VerificationInstruction) instrs.elementAt(loop);
            Debug_print1(specialInst.toStringSpecial());
            Debug_print1("---------------------------");
        }
    }

    public void printFramesOfTheWholeMethod(MethodInfo method, long instrId) {
        if (!shouldDebugPrint) {
            return;
        }
        Vector instrs = method.getCodeAtt().getInstructions();
        for (int loop = 0; loop < instrs.size(); loop++) {
            VerificationInstruction specialInst = (VerificationInstruction) instrs.elementAt(loop);
            if (specialInst.getInstructionId() == instrId) {
                Debug_print1(specialInst.toStringSpecial());
                Debug_print1("---------------------------");
            }
        }
    }

    protected boolean shouldMethodExecute(MethodInfo method, Vector localVariables,
            OperandStack callerStack) {
        //save the method status
        return true;
    }

    public static void clearAllMethodFrames() {
        Vector<CodeAttCache> codeAttCache = Oracle.getInstanceOf().getAllCodeAtt();
        Iterator<CodeAttCache> it = codeAttCache.iterator();
        while (it.hasNext()) {
            clearMethodOldFrames(it.next().getMethodInfo());
        }
    }

    private static void clearMethodOldFrames(MethodInfo method) {
        Vector instructions = method.getInstructions();
        if (instructions != null) {
            int size = instructions.size();
            for (int loop = 0; loop < size; loop++) {
                VerificationInstruction instr = (VerificationInstruction) instructions.elementAt(loop);
                instr.clear();
            }
        }
    }

    protected String methodKey(MethodInfo method) {
        return method.getKey() + ", " + method.getClassFile().getThisClass().intValueUnsigned();
    }

    protected void workBeforeInstructionExecuted(Vector callingParameters,
            MethodInfo method,
            VerificationInstruction instrGoingToExecute,
            OperandStack operandStack,
            LocalVariables localVariables) throws Exception {
        lastInstrExecuted = instrGoingToExecute;
    }

    protected void workAfterInstructionExecuted(MethodInfo method, Frame frame,
            Vector nextInstrId,
            VerificationInstruction currentInstr,
            Vector allInstruction, Vector methodCallingParamerters) throws Exception {
        //Step 4
        updateStackLocalVariables(nextInstrId, currentInstr, frame, allInstruction);
        currentInstr.addNextInstrsToBeExecutedRecord(nextInstrId, allInstruction);

    }

    private void printVisitedAndChangedInstructions(Vector<VerificationInstruction> instrVec) {
        Debug_print1("\n==================Start===================");
        for (int loop = 0; loop < instrVec.size(); loop++) {
            VerificationInstruction instr = instrVec.elementAt(loop);
            if (instr.isVisited() || instr.getChangeBit()) {
                Debug_print1("isVisited= " + instr.isVisited() + ", isChanged=" + instr.getChangeBit());
                Debug_print("instr", instr);
            }
        }
        Debug_print1("================End==================\n");
    }

    public void executeNonCatchedExceptions(MethodInfo currentMethod,
            HashSet<Integer> catchedException, Frame frame,
            Vector methodCallingParam) throws Exception {
        Vector methodInstr = currentMethod.getInstructions();
        Vector<ExceptionTableEntry> exceptTableEntry = currentMethod.getCodeAtt().getExceptions();
        for (int loop = 0; loop < exceptTableEntry.size(); loop++) {
            if (catchedException.contains(loop)) {
                continue;
            }
            ExceptionTableEntry expTbl = exceptTableEntry.elementAt(loop);
            long targetInstrId = expTbl.getHandlerPCInstrId();
            int entryCatchType = expTbl.getCatchType().intValueUnsigned();
            if (entryCatchType == 0) {
                entryCatchType = oracle.getClassInfoByName("java/lang/Exception", currentMethod.getClassFile().getConstantPool());
            }
            //VerificationInstruction instrAtStart = (VerificationInstruction) MethodInfo.findInstruction(expTbl.getStartPCInstrId(), methodInstr);
            VerificationInstruction instrAtEnd = (VerificationInstruction) MethodInfo.findInstruction(expTbl.getEndPCInstrId() - 1, methodInstr);
            Vector<Long> targetInstrIDs = new Vector();
            targetInstrIDs.addElement(targetInstrId);
            Vector<Integer> execptionClassesThisPointer = new Vector<Integer>();
            execptionClassesThisPointer.addElement(entryCatchType);
            /*executeRunTimeException(instrAtStart, currentMethod, frame,
            methodCallingParam, targetInstrIDs,
            execptionClassesThisPointer);*/
            executeRunTimeExceptionHelper(instrAtEnd, currentMethod, frame,
                    methodCallingParam, targetInstrIDs,
                    execptionClassesThisPointer);
            catchedException.add(loop);
        }

    }

    private void printLineNumberOfExceptionGenerated(String currentMethod,
            VerificationInstruction instrThatGernatesExep,
            Vector<Long> targetCatchInstrIds) {
        LineNumberController lineNumberContr = LineNumberController.getInstanceOf();
        int lineNumber = lineNumberContr.getLineNumberInfo(instrThatGernatesExep.getInstructionId());
        Debug_print("currentMethod=", currentMethod);
        Debug_print("exception produce from line number =", lineNumber);
        Iterator<Long> it = targetCatchInstrIds.iterator();
        while (it.hasNext()) {
            long lineNumberOfHandler = it.next();
            Debug_print("\t handler line number = ", lineNumberContr.getLineNumberInfo(lineNumberOfHandler));
        }

    }

    /**
     * It find the possible instruction that would be executed if current
     * instruction throw a run-time exeception. In case such
     * 
     * @param inst
     * @param currentMethod
     * @param frame
     * @param methodCallingParam
     * @param exceptionTableEntriedUsed
     * @throws Exception
     */
    protected void executeRunTimeException(VerificationInstruction inst,
            MethodInfo currentMethod,
            Frame frame, Vector methodCallingParam,
            HashSet exceptionTableEntriedUsed) throws Exception {
        boolean print = false;

        /**
         * Save the current class to a temp variable so that later on 
         * current class can be restored from the temp.
         */
        ClassFile oldClassFile = ClassFile.currentClassToWorkOn;
        if (print) {
            Miscellaneous.println(ClassFile.currentClassToWorkOn.getFullyQualifiedClassName() + " --- 1");
        }
        /**
         * Find the list of exception thrown by current instruction
         */
        ExceptionInfo excRecord = new ExceptionInfo(inst);
        ExceptionHandler.exceptionsThrownByAnInstruction(inst, currentMethod, excRecord);
        /**
         * If no exception is thrown by current instruction then we are done and return
         * after restoring current class pointer from temp variable.
         */
        if (excRecord.isEmpty()) {
            ClassFile.currentClassToWorkOn = oldClassFile;
            return;
        }
        /**
         * record the exception generated now in a global variable.
         * This record is used to generate exception never generated by any instr
         * at the end of method.
         */
        exceptionTableEntriedUsed.addAll(excRecord.getExceptionTableEntriedUsed());
        if (print) {
            Miscellaneous.println(ClassFile.currentClassToWorkOn.getFullyQualifiedClassName() + " --- 1");
        }
        /**
         * Knowing what exceptions are generated by current instruction now finds
         * the targetInstrIDs. These are the first instructions of a corresponding
         * catch blocks.
         */
        Vector<Long> targetInstrIDs = excRecord.getTargetCatchInstrIDs();

        printLineNumberOfExceptionGenerated(Oracle.getInstanceOf().getMethodOrFieldString(currentMethod),
                inst, targetInstrIDs);

        /**
         * Knowing what exceptions are generated by the current instruction now
         * finds the exception class ID. We have to make object of those classes.
         */
        Vector<Integer> execptionClassesThisPointer = excRecord.getExceptionClassesThisPointers();
        if (print) {
            Miscellaneous.println(ClassFile.currentClassToWorkOn.getFullyQualifiedClassName() + " --- 1");
        }
        executeRunTimeExceptionHelper(inst, currentMethod, frame, methodCallingParam,
                targetInstrIDs, execptionClassesThisPointer);
        if (print) {
            Miscellaneous.println(ClassFile.currentClassToWorkOn.getFullyQualifiedClassName() + " --- 1");
        }
        ClassFile.currentClassToWorkOn = oldClassFile;
    }

    protected void executeRunTimeExceptionHelper(VerificationInstruction inst,
            MethodInfo currentMethod,
            Frame frame, Vector methodCallingParam, Vector<Long> targetInstrIDs,
            Vector<Integer> execptionClassesThisPointer) throws Exception {
        /**
         * loop through all the target instr ids. 
         * These are the first instructions executed to be executed to handle
         * an exception that could be generate by an instruction.
         */
        for (int loop = 0; loop < targetInstrIDs.size(); loop++) {
            VerificationFrameFactory frameFactory = FrameFactoryPlaceHolder.getInstanceOf().getFactory();
            /*
             * Frame is set to a dummy stack
             * The stack is empty with only one element (exception) in it.
             * The reason we make a new dummy stack is because we have to return to the
             * normal execution and will need the normal stack.
             */
            OperandStack stack = frameFactory.createOperandStack(frame.getOperandStack().getMaxSize());
            int refType = execptionClassesThisPointer.elementAt(loop);
            if (refType <= 0) {
                continue;
            }
            Type type = frameFactory.createType(refType, true, -1);
            stack.push(type);
            Vector<Long> dummy = new Vector();
            dummy.addElement(targetInstrIDs.elementAt(loop));
            frame.updateFrame(stack);
            /**
             * Basically here we tell that next instruction to be executed
             * should be the instruction in the catch block. That instruction
             * is not "dirty" and will be selected for execution later on.
             * This is accomplish by passing the current instruction id 
             * as parameter to the following function.
             */
            workAfterInstructionExecuted(currentMethod, frame, dummy, inst,
                    currentMethod.getInstructions(), methodCallingParam);
        }

    }

    /**
     * It is possible that an implementation of a method called by 
     * current method invoke exception throw an exception whose catch 
     * block we have not visited. Unless we know exact method calls we
     * cannot visit all the call blocks. Hence this method process the code
     * inside a call block that is not called so far.
     *
     * @param inst
     * @param parentFunctionStack
     * @param currentMethod
     * @param frame
     * @param methodCallingParam
     * @param exceptionTableEntriedUsed
     * @throws Exception
     */
    public void excuteNonCalledExceptions(VerificationInstruction inst,
            OperandStack parentFunctionStack, MethodInfo currentMethod,
            Frame frame, Vector methodCallingParam,
            HashSet exceptionTableEntriedUsed) throws Exception {
    }

    protected void executeInstructions(BytecodeVerifier virtualInterpreter,
            OperandStack callerStack,
            Vector localVariables) throws
            Exception {
        MethodInfo method = virtualInterpreter.getMethodInfo();
        if (method.getInstructions() == null || method.getInstructions().isEmpty()) {
            return;
        }
        HashSet<Integer> excepTableEntriesUsed = excepTableEntriesUsedPerMethod.get(method);
        if (excepTableEntriesUsed == null) {
            excepTableEntriesUsed = new HashSet<Integer>();
            excepTableEntriesUsedPerMethod.put(method, excepTableEntriesUsed);
        }
        boolean isNonCachedExceptionExecuted = false;
        /*
         * EXECUTION
         * Step 1:
         */
        while (true) {
            lastBytecodeVerifier = virtualInterpreter;
            Frame frame = virtualInterpreter.getFrame();
            Vector methodInstrs = method.getCodeAtt().getInstructions();
            int index = selectInstructionToVerify(methodInstrs);
            if (index == -1) {
                if (!isNonCachedExceptionExecuted) {
                    executeNonCatchedExceptions(method, excepTableEntriesUsed, frame,
                            localVariables);
                    isNonCachedExceptionExecuted = true;
                    continue;
                }
                if (index == -1) {
                    /*should check for fall-out*/
                    return;
                } else {
                    /*
                     * Time to run code inside an exception handler that was
                     * not generated by any instruction.
                     */
                    continue;
                }
            }
            VerificationInstruction specialInst = (VerificationInstruction) methodInstrs.elementAt(index);
            specialInst.createStackLVForInstr(method.getCodeAtt());
            /*
             * now it has been visited and changed bit is false too
             */
            specialInst.setChangeBit(false);
            specialInst.setVisited(true);

            int address = specialInst.getOffSet();
            /*
             * updates the frame with stack saved in the instruction
             */
            frame.updateFrame(specialInst);

            Debug_print("\n\n\t" + ClassFile.currentClassToWorkOn.getFullyQualifiedClassName(),
                    oracle.getMethodOrFieldString(method));
            Debug_print("********* Inst:  ", address + ":\t");
            Debug_print(specialInst, " , stack=", specialInst.getOperandStack(), ", LV=",
                    specialInst.getLocalVariables());
            Debug_print("currentLineNumber =", LineNumberController.getInstanceOf().getLineNumberInfo(specialInst.getInstructionId()));

            if (oracle.getMethodOrFieldString(method).contains("java.io.PrintStream.print(I)V")
                    && specialInst.getInstructionId() == 34277
                    && specialInst.getMnemonic().contains("")
                    && specialInst.getLineNumber() >= 0) {
                Miscellaneous.println("Stop here+7 " + specialInst);
                shouldDebugPrint = true;
                if (shouldDebugPrint) {
                    printFramesOfTheWholeMethod(method, 9151);
                }
            }
            //Debug_print("instr order Id=", CreateInterMethodStrongConnCompID.getInstanceOf().getInterMethodStronglyConnectInstrId((GCInstruction) specialInst));
            workBeforeInstructionExecuted(virtualInterpreter.getMethodCallingParameters(),
                    method, specialInst,
                    frame.getOperandStack(),
                    frame.getLocalVariables());
            /*
             * Step 2 and Step 3
             */
            MultiplePoolsFacade pOne = specialInst.getMethod().getClassFile().getConstantPool();
            Vector<Long> nextInstructions = lastBytecodeVerifier.execute(pOne,
                    specialInst, address, callerStack);
            /*
             * Step 4 is inside following method
             */
            workAfterInstructionExecuted(method, frame, nextInstructions,
                    specialInst, methodInstrs, localVariables);
            Debug_print("\n\n\tOperandStack after execution ", frame.getOperandStack());
            Debug_print("\tLocalVariables after execution ", frame.getLocalVariables());

            Debug_print("\t Next instructions ", nextInstructions);
            executeRunTimeException(specialInst, method,
                    frame, localVariables, excepTableEntriesUsed);
            if (shouldDebugPrint) {
                Miscellaneous.println("Stop here 3");
                printFramesOfTheWholeMethod(method, 9151);
            }
            /*
             *Going back to Step 1
             */
        }
    }

    /**
     * It implements step-4 as described in class description.
     *
     * @param nextInstrsId
     * @param currentInstr
     * @param frame
     * @param allInst
     * @throws Exception
     */
    private void updateStackLocalVariables(Vector<Long> nextInstrsId,
            VerificationInstruction currentInstr,
            Frame frame,
            Vector allInst) throws Exception {
        VerificationInstruction inst = null;
        LocalVariables localVar = frame.getLocalVariables();
        OperandStack stack = frame.getOperandStack();
        boolean changed = true;
        for (int loop = 0; loop < nextInstrsId.size(); loop++) {
            long id = nextInstrsId.elementAt(loop);
            if (id == -1) {
                int nextInstOffset = currentInstr.getOffSet() + currentInstr.length();
                inst = (VerificationInstruction) MethodInfo.findInstruction(nextInstOffset,
                        allInst);
                nextInstrsId.remove(loop);
                nextInstrsId.add(loop, inst.getInstructionId());
            } else {
                inst = (VerificationInstruction) MethodInfo.findInstruction(id,
                        allInst);
            }
            //if already not visited then do the adding otherwise merge
            changed = true;
            if (inst.isVisited()) {
                Debug_print(">>>>>>>>>>>> merging with inst ", inst.toStringSpecial());
                changed = inst.merge(currentInstr, localVar, stack);
            } else {
                inst.set(localVar, stack);
                inst.setVisited(true);
            }
            if (changed) {
                inst.setChangeBit(changed);
            }
        }
    }

    /* 1. Select a virtual machine instruction whose "changed" bit is set. If no instruction
     *  remains whose "changed" bit is set, the method has successfully been verified.
     *  Otherwise, turn off the "changed" bit of the selected instruction.
     */
    private int selectInstructionToVerify(Vector instructions) {
        VerificationInstruction inst = null;
        int changeInstrIndex = -1;
        VerificationInstruction changeInstr = null;
        for (int loop = 0; loop < instructions.size(); loop++) {
            inst = (VerificationInstruction) instructions.elementAt(loop);
            if (inst.getChangeBit()) {
                changeInstrIndex = loop;
                changeInstr = inst;
                break;
            }
        }
        if (changeInstr != null) {
            inst.setChangeBit(false);
        }
        return changeInstrIndex; //end of verification
    }
}
